Termination of the given ITRSProblem could successfully be proven:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

eval_2(i, j) → Cond_eval_21(<=@z(j, -@z(i, 1@z)), i, j)
Cond_eval_2(TRUE, i, j) → eval_1(-@z(i, 1@z), j)
eval_2(i, j) → Cond_eval_2(>@z(j, -@z(i, 1@z)), i, j)
eval_1(i, j) → Cond_eval_1(>=@z(i, 0@z), i, j)
Cond_eval_21(TRUE, i, j) → eval_2(i, +@z(j, 1@z))
Cond_eval_1(TRUE, i, j) → eval_2(i, 0@z)

The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

eval_2(i, j) → Cond_eval_21(<=@z(j, -@z(i, 1@z)), i, j)
Cond_eval_2(TRUE, i, j) → eval_1(-@z(i, 1@z), j)
eval_2(i, j) → Cond_eval_2(>@z(j, -@z(i, 1@z)), i, j)
eval_1(i, j) → Cond_eval_1(>=@z(i, 0@z), i, j)
Cond_eval_21(TRUE, i, j) → eval_2(i, +@z(j, 1@z))
Cond_eval_1(TRUE, i, j) → eval_2(i, 0@z)

The integer pair graph contains the following rules and edges:

(0): COND_EVAL_1(TRUE, i[0], j[0]) → EVAL_2(i[0], 0@z)
(1): EVAL_2(i[1], j[1]) → COND_EVAL_2(>@z(j[1], -@z(i[1], 1@z)), i[1], j[1])
(2): EVAL_1(i[2], j[2]) → COND_EVAL_1(>=@z(i[2], 0@z), i[2], j[2])
(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(4): COND_EVAL_2(TRUE, i[4], j[4]) → EVAL_1(-@z(i[4], 1@z), j[4])
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(0) -> (1), if ((i[0] →* i[1]))


(0) -> (5), if ((i[0] →* i[5]))


(1) -> (4), if ((i[1] →* i[4])∧(j[1] →* j[4])∧(>@z(j[1], -@z(i[1], 1@z)) →* TRUE))


(2) -> (0), if ((i[2] →* i[0])∧(j[2] →* j[0])∧(>=@z(i[2], 0@z) →* TRUE))


(3) -> (1), if ((+@z(j[3], 1@z) →* j[1])∧(i[3] →* i[1]))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))


(4) -> (2), if ((j[4] →* j[2])∧(-@z(i[4], 1@z) →* i[2]))


(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): COND_EVAL_1(TRUE, i[0], j[0]) → EVAL_2(i[0], 0@z)
(1): EVAL_2(i[1], j[1]) → COND_EVAL_2(>@z(j[1], -@z(i[1], 1@z)), i[1], j[1])
(2): EVAL_1(i[2], j[2]) → COND_EVAL_1(>=@z(i[2], 0@z), i[2], j[2])
(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(4): COND_EVAL_2(TRUE, i[4], j[4]) → EVAL_1(-@z(i[4], 1@z), j[4])
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(0) -> (1), if ((i[0] →* i[1]))


(0) -> (5), if ((i[0] →* i[5]))


(1) -> (4), if ((i[1] →* i[4])∧(j[1] →* j[4])∧(>@z(j[1], -@z(i[1], 1@z)) →* TRUE))


(2) -> (0), if ((i[2] →* i[0])∧(j[2] →* j[0])∧(>=@z(i[2], 0@z) →* TRUE))


(3) -> (1), if ((+@z(j[3], 1@z) →* j[1])∧(i[3] →* i[1]))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))


(4) -> (2), if ((j[4] →* j[2])∧(-@z(i[4], 1@z) →* i[2]))


(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_EVAL_1(TRUE, i, j) → EVAL_2(i, 0@z) the following chains were created:




For Pair EVAL_2(i, j) → COND_EVAL_2(>@z(j, -@z(i, 1@z)), i, j) the following chains were created:




For Pair EVAL_1(i, j) → COND_EVAL_1(>=@z(i, 0@z), i, j) the following chains were created:




For Pair COND_EVAL_21(TRUE, i, j) → EVAL_2(i, +@z(j, 1@z)) the following chains were created:




For Pair COND_EVAL_2(TRUE, i, j) → EVAL_1(-@z(i, 1@z), j) the following chains were created:




For Pair EVAL_2(i, j) → COND_EVAL_21(<=@z(j, -@z(i, 1@z)), i, j) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(<=@z(x1, x2)) = -1   
POL(0@z) = 0   
POL(TRUE) = -1   
POL(EVAL_1(x1, x2)) = -1 + x1   
POL(FALSE) = -1   
POL(>@z(x1, x2)) = -1   
POL(>=@z(x1, x2)) = -1   
POL(EVAL_2(x1, x2)) = -1 + x1   
POL(COND_EVAL_1(x1, x2, x3)) = -1 + x2   
POL(COND_EVAL_2(x1, x2, x3)) = -1 + x2   
POL(COND_EVAL_21(x1, x2, x3)) = -1 + x2   
POL(+@z(x1, x2)) = x1 + x2   
POL(1@z) = 1   
POL(undefined) = -1   

The following pairs are in P>:

COND_EVAL_2(TRUE, i[4], j[4]) → EVAL_1(-@z(i[4], 1@z), j[4])

The following pairs are in Pbound:

COND_EVAL_1(TRUE, i[0], j[0]) → EVAL_2(i[0], 0@z)

The following pairs are in P≥:

COND_EVAL_1(TRUE, i[0], j[0]) → EVAL_2(i[0], 0@z)
EVAL_2(i[1], j[1]) → COND_EVAL_2(>@z(j[1], -@z(i[1], 1@z)), i[1], j[1])
EVAL_1(i[2], j[2]) → COND_EVAL_1(>=@z(i[2], 0@z), i[2], j[2])
COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

At least the following rules have been oriented under context sensitive arithmetic replacement:

-@z1 ↔
+@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
                ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(1): EVAL_2(i[1], j[1]) → COND_EVAL_2(>@z(j[1], -@z(i[1], 1@z)), i[1], j[1])
(2): EVAL_1(i[2], j[2]) → COND_EVAL_1(>=@z(i[2], 0@z), i[2], j[2])
(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(4): COND_EVAL_2(TRUE, i[4], j[4]) → EVAL_1(-@z(i[4], 1@z), j[4])
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(3) -> (1), if ((+@z(j[3], 1@z) →* j[1])∧(i[3] →* i[1]))


(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))


(4) -> (2), if ((j[4] →* j[2])∧(-@z(i[4], 1@z) →* i[2]))


(1) -> (4), if ((i[1] →* i[4])∧(j[1] →* j[4])∧(>@z(j[1], -@z(i[1], 1@z)) →* TRUE))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
                ↳ IDependencyGraphProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z)) the following chains were created:




For Pair EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(<=@z(x1, x2)) = -1   
POL(EVAL_2(x1, x2)) = -1 + (-1)x2 + x1   
POL(TRUE) = -1   
POL(COND_EVAL_21(x1, x2, x3)) = -1 + (-1)x3 + x2   
POL(+@z(x1, x2)) = x1 + x2   
POL(FALSE) = -1   
POL(1@z) = 1   
POL(undefined) = -1   

The following pairs are in P>:

COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))

The following pairs are in Pbound:

COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))

The following pairs are in P≥:

EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
                ↳ IDependencyGraphProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])


The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): COND_EVAL_1(TRUE, i[0], j[0]) → EVAL_2(i[0], 0@z)
(1): EVAL_2(i[1], j[1]) → COND_EVAL_2(>@z(j[1], -@z(i[1], 1@z)), i[1], j[1])
(2): EVAL_1(i[2], j[2]) → COND_EVAL_1(>=@z(i[2], 0@z), i[2], j[2])
(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(2) -> (0), if ((i[2] →* i[0])∧(j[2] →* j[0])∧(>=@z(i[2], 0@z) →* TRUE))


(3) -> (1), if ((+@z(j[3], 1@z) →* j[1])∧(i[3] →* i[1]))


(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))


(0) -> (1), if ((i[0] →* i[1]))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))


(0) -> (5), if ((i[0] →* i[5]))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDependencyGraphProof
                  ↳ IDP
                    ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))
(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

(5) -> (3), if ((i[5] →* i[3])∧(j[5] →* j[3])∧(<=@z(j[5], -@z(i[5], 1@z)) →* TRUE))


(3) -> (5), if ((+@z(j[3], 1@z) →* j[5])∧(i[3] →* i[5]))



The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z)) the following chains were created:




For Pair EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(<=@z(x1, x2)) = -1   
POL(EVAL_2(x1, x2)) = -1 + (-1)x2 + x1   
POL(TRUE) = 1   
POL(COND_EVAL_21(x1, x2, x3)) = -1 + (-1)x3 + x2   
POL(+@z(x1, x2)) = x1 + x2   
POL(FALSE) = -1   
POL(1@z) = 1   
POL(undefined) = -1   

The following pairs are in P>:

COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))

The following pairs are in Pbound:

COND_EVAL_21(TRUE, i[3], j[3]) → EVAL_2(i[3], +@z(j[3], 1@z))

The following pairs are in P≥:

EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDependencyGraphProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(5): EVAL_2(i[5], j[5]) → COND_EVAL_21(<=@z(j[5], -@z(i[5], 1@z)), i[5], j[5])


The set Q consists of the following terms:

eval_2(x0, x1)
Cond_eval_2(TRUE, x0, x1)
eval_1(x0, x1)
Cond_eval_21(TRUE, x0, x1)
Cond_eval_1(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.